k:Knd. (islocal(k))  (act(k)  Id) 

latex

Definitions	x:A. B(x), Knd, P  Q, islocal(k), t  T, act(k), prop{i:l}
Lemmas	outr wf, IdLnk wf, Id wf, assert wf, bnot wf, isl wf